Lemma false_implies_anything:
  forall a, false = true -> a.
Proof.
  intros.
  discriminate.
Qed.
